($i$)$\mathbb{Z}${-}det{-}fun($j$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$(if ($i$ =$_{0}$ 0) then $j$ else $i$ rem $j$ fi  =$_{0}$ 0)